0.00/0.31	MAYBE
0.00/0.31	
0.00/0.31	Problem:
0.00/0.31	 app (lam (\x. M (var x))) N -> M N
0.00/0.31	
0.00/0.31	Proof:
0.00/0.31	 Open
0.00/0.31	EOF